\section{Lifting \gmtoautosar}
\label{section:lifting_dsltrans}

\subsection{Background: DSLTrans}
\label{subsec:dsltrans}
DSLTrans is an out-place, graph-based and rule-based model transformation engine
that has two important properties enforced by construction: all its computations
are both \emph{terminating} and \emph{confluent}~\cite{BarrocaLAFS10}. Besides
their obvious importance in practice, these two properties were instrumental in
the implementation of a verification technique for pre- / post-condition
properties that can be shown to hold for all executions of a given DSLTrans
model transformation, independently of the provided input
model~\cite{Lucio:10,LOH+14,selimICGT2014}. 

Model transformations are expressed in DSLTrans as sets of graph rewriting
rules, having the classical left- and right-hand sides and, optionally, negative
application conditions. The scheduling of model transformation rules in DSLTrans
is based on the concept of \emph{layer}. Each layer contains a set of model
transformation rules that execute independently from each other. Layers are
organized sequentially and the output model that results from executing a given
layer is passed to the next layer in the sequence. A DSLTrans rule can match
over the elements of the input model of the transformation (that remains
unchanged throughout  the entire execution of the transformation) but also over
elements that have been generated so far in the output model. The independence
of the execution of rules belonging to the same layer is enforced by allowing
matching over the output of rules from previous layer but not over the output
of rules of the current layer. Matching over elements of the output model of a
transformation is achieved using a DSLTrans construct called \emph{backward
links}. Backward links allow matching over traces between elements in the input
the output models of the transformation. These traces are explicitly built by
the DSLTrans transformation engine during rule execution. 

\begin{figure}[t]
  \begin{center}
    \includegraphics[width=0.8\textwidth]{imgs/rule.pdf} 
    \caption{The \emph{CreatePPortPrototype} rule in the \gmtoautosar DSLTrans transformation.}
    \label{fig:DSLTrans_rule}
  \end{center}
  %\vspace{-0.35in}
\end{figure}

For example, we depict in Fig.~\ref{fig:DSLTrans_rule} the \emph{CreatePPortPrototype} rule
in the \gmtoautosar DSLTrans transformation, previously introduced in
Table~\ref{tab:rulesPerLayer}. The rule is comprised of a \emph{match} and an
\emph{apply} part, corresponding to the usual left- and right-hand sides in
graph rewriting. When a rule is applied, the graph in the match part of the rule
is looked for in the transformation's input model, together with the match
classes in the apply part of the rule that are connected to \emph{backward
links}. An example of a \emph{backward link} can be observed in
Fig.~\ref{fig:DSLTrans_rule}, connecting the \emph{CompositionType} and the
\emph{PhysicalNode} match classes. During the rewrite part of rule application,
the instances of classes in the apply part of the rule that are not connected to
backward links, together with their adjacent relations, are created in the
output model. In the example in Fig.~\ref{fig:DSLTrans_rule}, the
\emph{CreatePPortPrototype} rule creates a \emph{PPortPrototype} object and a
\emph{port} relation per matching site found. 
Note that the vertical arrow
between the \emph{shortName} attribute of \emph{PPortPrototype} and the
\emph{name} attribute of \emph{ExecFrame} implies that the value of attribute
\emph{name} is copied from its matching site to the \emph{shortName} attribute
of the\emph{PPortPrototype} instance created by the rule.  

In addition to the constructs presented in the example in
Fig.~\ref{fig:DSLTrans_rule}, DSLTrans has several others: \emph{existential matching}
which allows selecting only one result when a match class of a rule matches an input
model, \emph{indirect links} which allow transitive matching over containment
relations in the input model, and \emph{negative application conditions} which allow
 to specify conditions under which a rule should not match, as usual. The
\gmtoautosar transformation does not make use of these constructs, and thus
we leave the problem of lifting them for future work.
 
 
% As mentioned in Sec.~\ref{subsec:model_transformations}\mf{FIXME}, the majority of the
% languages in which model transformations are written have the same
% expressiveness as any general purpose programming language. This fact implies the advantage
% that, in theory, any computation that can be described in any programming
% language can also be described using a model transformation.
% DSLTrans~\cite{BarrocaLAFS10} is a model transformation language that
% is specialized to a particular kind of computation -- for the purpose of this
% discussion we will broadly call this class of computations \emph{translations}.
% \emph{Translations} include all computations that have as goal the generation of
% a new model from an input model. Because model transformations are heavily used in
% the context of Model-Driven Development (MDD)~\cite{Sendall2003}, these
% computations are in general related to software development. Concrete examples
% are \emph{code generation}, \emph{refinement}, \emph{reverse engineering},
% \emph{migration}, among several others that have been described
% in~\cite{LAD+2014}. Such computations have the interesting properties that they
% always \emph{terminate} (otherwise they are not meaningful) and are nearly
% always required to be \emph{deterministic} (or can be reduced to the
% deterministic computation of a set of results)\rs{but most transformations (refactorings, abstractions,etc.) have these properties --
% it doesn't seem too specific to translations}. DSLTrans specializes for
% \emph{translations} by enforcing these two properties by construction. In other
% words, any model transformation described in DSLTrans is guaranteed to terminate
% and to be deterministic~\cite{BarrocaLAFS10} because of the way in which
% DSLTrans is defined. In order to guarantee these two properties, the
% expressiveness of DSLTrans is lower than that of a general-purpose programming
% language. Two restrictions are noteworthy: 1) no loops with arbitrary stop
% conditions are allowed; and 2) we enforce that transformation rules in a
% DSLTrans transformation are divided in layers that execute sequentially. \rs{These
% are sufficient restrictions to enforce the props but they are not necessary. So you 
% might want to phrase things differently (Also I think
% the exact set of restrictions is undecidable due to the undecidability of the 
% halting problem.)}The
% rules that compose each of those layers are guaranteed to execute independently
% and in parallel from each other.
% 
% The expressiveness restrictions present in DSLTans also impose some limitations
% on its usage. The most important one is that, because looping is essentially \rs{clarify 'essentially'} not
% allowed, computations modeling reactive systems cannot be expressed in DSLTrans.
% The behavior of such systems can be described by using model transformation
% rules as the means to update the system's state, thus effectively modeling its
% operational semantics. Model transformations of this kind have been named
% \emph{simulations} in~\cite{LAD+2014}. 
% 
% Despite these limitations, there are multiple advantages to a restricted model transformation
% language such as DSLTrans. On the one hand, it is often the case for more
% expressive transformation languages that properties such as \emph{termination}
% and \emph{determinism}  need to be statically checked on transformations
% written in those
% languages~\cite{EhrigEhrigTaentzerdeLaraVarroVarro2005,J:Lambers-etAl-2006}. On
% the other hand, and more importantly in the context of this paper, such
% restrictions have allowed for the development of a verification technique for
% DSLTrans model transformations~\cite{Lucio:10}. This verification technique
% allows guaranteeing pre/post-condition properties for all executions of a
% DSLTrans model transformation by using a static symbolic execution-like
% technique~\cite{LOH+14}. More precisely we are able to guarantee that, for all
% potential (infinite) executions of a given DSLTrans model transformation, if a
% certain pattern appears in the transformation's input model, then a corresponding
% pattern will appear in the transformation's output model. We have been able to
% demonstrate the applicability and efficiency of our verification technique when
% analyzing a case study transformation extracted from General
% Motors~\cite{selimICGT2014}. 
% 
% 
% 
% What does it take to produce a lifted version of DSLTrans \rs{unfinished sentence}

% 

\subsection{Lifting DSLTrans for \gmtoautosar}

\subsubsection{Lifting of Production Rules.} 
When executing a DSLTrans transformation, the basic operation (called here a
{\em ``production''}) is the application of a individual rule at a particular
matching site. The definition and theoretical foundation of lifting for
productions are given  in \cite{salay14}.  Below, we describe how they apply in
the case of \gmtoautosar using the model fragment in Fig.~\ref{fig:toyexample}
and the \emph{CreatePPortPrototype} rule in Fig.~\ref{fig:DSLTrans_rule}.

When a DSLTrans rule $R$ is lifted, we denote it by $\lifted{R}$.
Intuitively, the meaning of a $\lifted{R}$-production is that it should result
in a product line with the same products as we would get by applying $R$ to 
all the products of the original product line at the same site. Because of this,
we do not expect a $\lifted{R}$-production to affect the set of allowable
feature combinations in the product line. 
Formally:


\BD [Correctness of lifting a production] 
\label{def:correctness}
Let a rule $R$ and a product line $P$, and a matching site $c$ be given.
$\lifted{R}$ is a \emph{correct lifting} of $R$
iff 
(1) if $P \apply{\lifted{R}|c} P'$ then
% for all \emph{rule applications} $P \apply{\lifted{R}} P'$,
$\mathsf{Conf}(P') = \mathsf{Conf}(P)$, and 
(2) for all configurations $\mathsf{Conf}(P)$,
$M \apply{R|c} M'$, where $M$ can be derived from $P$ and $M'$ from $P'$ under
the same configuration.
\ED

An algorithm for applying lifted rules at a specific site is given
in \cite{salay14}, along with a proof of production correctness that is
consistent with the above definition.
In brief, given a matching site and a lifted rule, the algorithm performs the
following steps:
\begin{inparaenum}[(a)]
\item use a SAT solver to check whether the rule is applicable to at least one
product at that site,
\item modify the domain model of the product line, and 
\item modify the presence conditions of the changed domain model so the rule
effect only occurs in applicable products.
\end{inparaenum}

For example, consider the match c=\{\emph{BodyControl},
\emph{HumanMachineInterface}, \emph{Display}, \emph{De\_ActivateACC},
\emph{TurnABSoff}, \emph{BodyControlCT}\} in the fragment in
Fig.~\ref{fig:toyexample}. In this match, we assume that an element named
\emph{BodyControlCT} of type \emph{CompositionType} and its corresponding
backward link have been previously created by the rule
\emph{MapPhysNode2FiveElements} (see Table~\ref{tab:rulesPerLayer})
and therefore have the presence condition $F2 \vee F3$. 
To apply the rule ${\lifted{\mbox{\emph{CreatePPortPrototype}}}}$ to $c$, 
we first need check whether all of $c$ is fully present in at least one product.
We do so by checking whether the formula $\Phi_{apply}=(F2\vee
F3)\wedge(F8\vee F3)$ is satisfiable.  $\Phi_{apply}$ is constructed by
conjoining the presence conditions of all the domain elements in the matching
site $c$. According to the general lifting algorithm in \cite{salay14}, 
the construction of $\Phi_{apply}$  for arbitrary graph transformation rules is
more complex; however, rules in \gmtoautosar do not use Negative
Application Conditions and do not cause the deletion of any domain element.
Therefore, the construction of $\Phi_{apply}$  follows the pattern we described
for all rules
in \gmtoautosarlifted.

Because $\Phi_{apply}$  is satisfiable,
${\lifted{\mbox{\emph{CreatePPortPrototype}}}}$ is applicable at $c$. Therefore,
the rule creates
a new element called \emph{De\_ActivateACC} of type \emph{PPortPrototype}, a
link of type \emph{port} connecting it to \emph{BodyControlCT}, as well as the
appropriate backward links. Finally, all created elements are assigned
$\Phi_{apply}$ as their presence condition. In other words, the added presence
conditions ensure that the new elements will only be part of products for which
the rule is applicable.  By construction, 
this production satisfies the correctness condition in
Def.~\ref{def:correctness}.  
Thus,  according to the proofs in \cite{salay14}, the
lifting of productions preserves confluence and termination.


\subsubsection{Lifting the Transformation.} 
We define the notion of global correctness for \gmtoautosarlifted to
mean that, given an input product line of GM models, it should produce a product
line of AUTOSAR models that would be the same as if we had applied \gmtoautosar
to each GM model individually:

\BD [Global Correctness of \gmtoautosarlifted] 
\label{def:globalCorrectness}
The transformation \gmtoautosarlifted is \emph{correct} iff for any input product line
$P$, it produces a product line $P'$ such that
(a) $\mathsf{Conf}(P) = \mathsf{Conf}(P')$, and 
(b) for all configurations $\mathsf{Conf}(P)$,  $M'=\gmtoautosar(M)$,
where $M$ and $M'$ can be derived from $P$ and $P'$, respectively, under the
same configuration.
\ED

In order to lift \gmtoautosar, we use the DSLTrans engine to perform the
identification of matching sites and scheduling of individual productions, and
use the lifting algorithm in \cite{salay14} to lift individual productions, as
described above.  Since each production is correct with respect to
Def.~\ref{def:correctness}, then, by transitivity, the lifted version
\gmtoautosarlifted is globally correct. Also by transitivity, since the lifting of
individual productions preserves confluence and termination, it
is confluent and terminating, like \gmtoautosar.
%
Because of global correctness, and because it preserves confluence and
termination, \gmtoautosarlifted also preserves the results of the verification
of pre- and post-condition properties using the techniques
in \cite{Lucio:10,LOH+14,selimICGT2014}. In other words, \gmtoautosarlifted
satisfies the same set of pre- and post-condition properties as \gmtoautosar.


\subsubsection{Implementation.}
Adapting the DSLTrans engine for \gmtoautosarlifted required adding functionality to the
existing codebase. We had to write code to extend it to enable the following functionality: 
\begin{inparaenum}[(a)]
\item Reading and writing presence conditions from and to secondary storage, expressed as 
Comma-Separated Values (CSV) and attach them in memory to EMF~\cite{gronback09} models.
\item Interfacing with the API of the Z3 SMT solver~\cite{z3}, used for checking
the satisfiability of $\Phi_{apply}$.
\item Associating presence conditions to elements belonging to the output model of the transformation and updating those presence condition as the transformation unfolds.
\end{inparaenum}
These changes required an addition of less than 300 lines of code to an existing
codebase of 9250 lines.

% 
% 
% 
% 
% 
% 
% \subsubsection{How is DSLTrans implemented.}
% \begin{itemize}
%   \item EMF models as input
%   \item Java implementation with a Prolog bridge for the queries to the model
%   \item Prolog is used to simplify matching elements in the model by using in-built backtracking capabilities~\cite{Schatz10}.
% \end{itemize}
% 
% \subsubsection{Implementation of lifting in DSLTrans.}
% 
% \begin{enumerate}
% \item Add the presence database which exists in parallel to the EMF model as a csv file. The presence database is loaded simultaneously with the EMF model and the presence conditions are associated by name and type to the elements in the model.
% \item Matching rules in the model in the original DSLTrans implementation is achieved using Prolog queries. These queries are such that all solutions to the matching of a rule are returned for all AnyMatchClass match elements and only one solution for ExistsMatchClass match elements. We have modified the query such that all elements are returned, independently of the type of the match element. This is needed because presence conditions need to exclude features for other possibilities of matching for exists elements\ldots (elaborate on this)
% \item A procedure for building Z3 expressions was implemented, both for passing the propositional logic formulas to the Z3 engine and to attach them to the elements produced by the transformation.
% \end{enumerate}
% 
